T, T':Type{i}, f:(TT'), L:T List, P:(T'T'Prop{i'}).
(x,ymap(f;L).P(x,y))  (x,yL.P(f(x),f(y))) 

latex

Definitions	P  Q, P  Q, x,y. t(x;y), Prop, (x,yL.P(x;y)), map(f;as), Top, i  j < k, AB, P & Q, A, False, P  Q, x(s1,s2), ||as||, {i..j}, x:A. B(x), t  T
Lemmas	int seg wf, length wf1, length-map, le wf, pairwise wf, map wf, select-map